COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	unique[f83,jmc]		The unique names assumption
C00004 00003		Perhaps A(Joe,Henry) should include ∃x y.x ≠ y or even
C00006 00004		Perhaps the most straightforward approach to the unique
C00011 00005	How about the axiom
C00013 00006	"reiter%ubc"@csnet-Relay
C00018 ENDMK
C⊗;
unique[f83,jmc]		The unique names assumption

	Ray Reiter pointed out that the treatment proposed in
my letter to him didn't work.  Here's another try.

Suppose we want to conclude that Joe is different from Henry if
this is permitted by some knowledge A(Joe,Henry) that we are
taking into account.  We circumscribe the expression

	Joe = Henry

regarding Joe and Henry as variable - not taking
equality to be variable as previous
attempts tried to.  We get

(1)	A(Joe,Henry) ∧ 
	(∀Joe' Henry'.A(Joe',Henry') ∧ (Joe' = Henry' ⊃ Joe = Henry)
		⊃ (Joe = Henry ≡ Joe' = Henry')).

If the language contains constants  Joe0  and  Henry0  which are provably
distinct and such that  A(Joe0,Henry0)  is provable, then we can
substitute these individuals for  Joe'  and  Henry'.
The left side of (1) is then true, and we can conclude  Joe ≠ Henry.

This is a great simplification of our previous attempts, because
we don't have to bother with names as objects and denotation
as a function.  Nevertheless, finding the desired constants  Joe0
and  Henry0  may not always be feasible.  Indeed it may beg the
question.

	Perhaps A(Joe,Henry) should include ∃x y.x ≠ y or even
∃x y.person(x) ∧ person(y) ∧ x ≠ y.  This wouldn't suffice if
we had ten individuals and were expected to jump to the conclusion
that they are all distinct.  We would need a stronger axiom
asserting the existence of enough individuals of the desired
kind.

	This sort of works for inferring that two specific objects
are distinct if possible.  However, suppose we have a whole collection
of objects, and we want as many as possible to be distinct.  Extending
the above method to four objects gives a six way parallel circumscription
which is reducible to a single circumscription by Lifschitz's
trick - namely we circumscribe  E(x,z) defined by

	(z = 1 ∧ x1 = x2) ∨ (z = 2 ∧ x1 = x3) ∨ (z = 3 ∧ x2 = x3) ∨
(z = 4 ∧ x1 = x4) ∨ (z = 5 ∧ x2 = x4) ∨ (z = 6 ∧ x2 = x4)

as a predicate of z with x1, x2, . . . ,x6 variable.  We have

A(x1, ... ,x6) ∧ ∀x1' ... x6'.A(x1',...x6') ∧ (∀z.E(x',z) ⊃ E(x,z))
		⊃(∀z.E(x,z) ≡ E(x',z))
	Perhaps the most straightforward approach to the unique
names hypothesis  involves taking the names themselves as objects.
The following is taken from a draft written before Reiter pointed
out that the approach proposed doesn't quite work.
circum[f83,jmc]		AI Aplications of Circumscription

#. The unique names hypothesis

	Raymond Reiter (1979) introduced the phrase "unique names hypothesis"
for the assumption that distinct names denote distinct objects.  We want
to show how to handle this in a more general way by circumscription.

	Suppose we introduce names as objects, i.e. we introduce
⊗'John as a name for John.  For brevity we use the Lisp notation
⊗'John instead of the more usual "John".  We then assume an infinity
of first order axioms like

	%2'John ≠ 'Henry%1,

i.e. for every pair of distinct names there is such an axiom.

	From the
point of view of mathematical logic, there is no harm in having
an infinity of such axioms.  From the computational point of view of
a theorem proving or problem solving program, we
merely suppose that we rely on the computer to generate the assertion
that two names are distinct whenever this is required, since
a subroutine can easily tell whether two strings are the same.

	[One might suppose that some metamathematical considerations would
change from using an infinity of axioms, but usually this won't
be so, because we can generate an infinity of provably distinct
objects from a finite set of axioms.  All we need do is use
integers as names, axiomatize > as a relation including its
transitivity and have an axiom %2∀x_y.x_>_y_⊃_x_≠_y%1.  It is equally
feasible to finitely axiomatize strings in a way that ensures that
distinct strings are provably distinct.  The axiom systems required
can be much weaker than Peano arithmetic, since induction is not
required to prove particular instances of inequality.]

	One way of getting unique names is to use axioms like

!!a2:	%2name(John) = 'John%1

and

	%2name(Henry) = 'Henry%1.

The distinctness of names and the theory of inequality will then
give %2John_≠_Henry%1.

	However, this is too absolute for many applications.  It is
often preferable that objects denoted by distinct
names are to be presumed distinct unless there is reason to believe
them to be the same.  We can do this as follows.  Instead of
using axioms like ({eq a2}), we write

!!a3:	%2denotation('John) = John%1

and

	%2denotation('Henry) = Henry%1

Nothing now prevents  %2John = Henry%1, so we use the axiom

!!a4:	%2∀n1 n2. n1 ≠ n2 ∧ ¬ab aspecteq(n1,n2) ⊃ denotation n1 ≠ denotation n2%1.

	The idea of this axiom is that if ⊗n1 and ⊗n2 are distinct names,
and ⊗aspecteq(n1,n2) is not abnormal, i.e. does not satisfy the predicate
⊗ab, then ⊗n1 and ⊗n2 denote distinct objects.  When we have "taken into
account" all the facts we are going to take into account we will circumscribe
the expression  %2ab_z%1.  This will make %2ab_aspecteq(n1,n2)%1 false
unless some facts prevent it and hence will allow inferring that
 %2denotation_n1%1 and
%2denotation_n2%1 are distinct unless there is evidence that they are equal.

.skip 1
How about the axiom
¬ab aspect1 n ⊃ name den n = n.

Then if the names are different, the objects they denote will be
different unless something is abnormal.

What is considered to be variable?  Most likely it should be the
function  name.

Here's a try

'a ≠ 'b

den 'a = a

den 'b = b

We circumscribe  ab z  with  ab  and  name  as variable.  This gives

'a ≠ 'b ∧ den 'a = a ∧ den 'b = b ∧ ∀n.¬ab aspect1 n ⊃ name den n = n

∧ ∀name' ab'.((∀n.¬ab' aspect1 n ⊃ name' den n = n)
	      ∧ ∀z. ab' z ⊃ ab z
	      ⊃ ∀z.ab z ⊃ ab' z).

This doesn't work unless  a  and  b  are variable too.  Actually, den
must be variable.

Kreisel points out that the common assumption in geometry that
a collection of points is in generic position may be taken as
a non-monotonically generated hypothesis.  I suppose this would
also apply to the notion of generic model of an axiom system
as introduced in discussions of forcing.  I would conjecture that
if Etherington is right that equality cannot be handled by circumscription,
then genericity can't either.
"reiter%ubc"@csnet-Relay
generalizing the unique names problem

The "unique names problem" is the following.  Some constant symbols,
a, b, etc. are constrained by an axiom  A.  We want to find
a general way of constructing a formula  UN(A), very likely
of second order logic, such that in the models of UN(A) maximize
inequality of a, b, etc.  It now seems unlikely that this
can be accomplished by circumscribing some formula.

Maybe "unique names" isn't an informative name for the problem.
Perhaps we should call it the "distinctness problem" or the
"problem of expressing a presumption of distinctness".

It may be worthwhile to think about a generalization of the problem.

There are some related mathematical concepts.  In geometry
one speaks about a figure being in general position provided the
co-ordinates of distinguished points satisfy no algebraic relations
not implied by its definition.  Thus a right triangle in general
position is not isosceles but also no side has twice
the length of another.  Indeed the sides satisfy
no algebraic equations other than  x↑2 + y↑2 = z↑2.  In algebraic
geometry one speaks of a generic point of an algebraic variety.
Again it is one that satisfies no relations other than those implied
by the fact that it is a point of the variety.  If the field is the
complex numbers and the variety is irreducible, i.e. isn't the union
of two or more varieties, then generic points exist.  If the field
is, for example, the rationals they need not exist, but can be shown
to exist in a suitable transcendental extension field.  For example,
(2t/(1+t↑2), (1 - t↑2)/(1 + t↑2)) is a generic point of x↑2 + y↑2 = 1.

In the theory of forcing, one speaks of a generic set.  This is a set
of natural numbers such neither it nor its complement contain any
infinite recursively enumerable sets, i.e. it has no special properties
other than finite ones.  This example probably isn't on the right
track for us, because we are primarily interested in finite systems.

	I am not an expert on any of the above-mentioned mathematical
concepts, but I think they suggest something to us.  Here is an
direct generalization of unique names.  We have an axiom  A.
We are interested in finding a wff  GCU(A) (for generalized circumscription,
unique) which distinguish those models in which as few terms as
possible are assigned equal value.  There will be two cases.  In the
first case, analogous to an irreducible variety or to the existence
of a unique minimal model with circumscription, GCU(A) will insure
that two terms are inequal unless this is implied by  A.  In the
more general case, e.g. when  A  is  x=y or w= z, there will be
a disjunction (possibly infinite).  The generalization consists
in allowing arbitrary ground terms and not just constants.

	It is by no means clear that GCU(A) exists as a
higher order formula systematically derivable from A, let alone
being obtainable by circumscription.  Maybe
it sometimes exists.  Maybe the idea of a generic point of a
variety can be taken over directly.